Inference at * 
Iof proof for Lemma equiv rel iff:


  EquivRel(;A,B.A  B) 

latex

 by Unfold `equiv_rel` 0 

latex

 1: 

 1:   Refl(;A,B.A  B) & Sym(;A,B.A  B) & Trans(;A,B.A  B)
 .

Definitions

EquivRel(T;x,y.E(x;y))